Nuprl Lemma : safety_nil
4,23
postcript
pdf
T
:Type,
P
:((
T
List)
Prop). (
l
:
T
List.
P
(
l
))
safety(
T
;
x
.
P
(
x
))
P
(nil)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Prop
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
l1
l2
,
safety(
A
;
tr
.
P
(
tr
))
,
{
T
}
Lemmas
nil
iseg
,
iseg
wf
origin
T:Type, P:((T List)
Prop). (
l:T List. P(l)) 
safety(T;x.P(x)) P(nil) T:Type, P:((T List)Prop). (l:T List. P(l)) safety(T;x.P(x)) P(nil) x:A. B(x)
T Qx:A. B(x)
l2